H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.93 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sortBy :: (a -> a -> Ordering) -> [a] -> [a]) :: (a -> a -> Ordering) -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sortBy :: (a -> a -> Ordering) -> [a] -> [a]

sortBy

cmp l

mergesort cmp l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sortBy :: (a -> a -> Ordering) -> [a] -> [a]) :: (a -> a -> Ordering) -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sortBy :: (a -> a -> Ordering) -> [a] -> [a]

sortBy

cmp l

mergesort cmp l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sortBy :: (a -> a -> Ordering) -> [a] -> [a]) :: (a -> a -> Ordering) -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sortBy :: (a -> a -> Ordering) -> [a] -> [a]

sortBy

cmp l

mergesort cmp l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sortBy :: (a -> a -> Ordering) -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sortBy :: (a -> a -> Ordering) -> [a] -> [a]

sortBy

cmp l

mergesort cmp l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sortBy",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sortBy vz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="sortBy vz3 vz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="mergesort vz3 vz4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="(mergesort' vz3) . map wrap",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="mergesort' vz3 (map wrap vz4)",fontsize=16,color="burlywood",shape="box"];572[label="vz4/vz40 : vz41",fontsize=10,color="white",style="solid",shape="box"];7 -> 572[label="",style="solid", color="burlywood", weight=9];
572 -> 8[label="",style="solid", color="burlywood", weight=3];
573[label="vz4/[]",fontsize=10,color="white",style="solid",shape="box"];7 -> 573[label="",style="solid", color="burlywood", weight=9];
573 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="mergesort' vz3 (map wrap (vz40 : vz41))",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' vz3 (map wrap [])",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="mergesort' vz3 (wrap vz40 : map wrap vz41)",fontsize=16,color="burlywood",shape="box"];574[label="vz41/vz410 : vz411",fontsize=10,color="white",style="solid",shape="box"];10 -> 574[label="",style="solid", color="burlywood", weight=9];
574 -> 12[label="",style="solid", color="burlywood", weight=3];
575[label="vz41/[]",fontsize=10,color="white",style="solid",shape="box"];10 -> 575[label="",style="solid", color="burlywood", weight=9];
575 -> 13[label="",style="solid", color="burlywood", weight=3];
11[label="mergesort' vz3 []",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' vz3 (wrap vz40 : map wrap (vz410 : vz411))",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="mergesort' vz3 (wrap vz40 : map wrap [])",fontsize=16,color="black",shape="box"];13 -> 16[label="",style="solid", color="black", weight=3];
14[label="[]",fontsize=16,color="green",shape="box"];15[label="mergesort' vz3 (wrap vz40 : wrap vz410 : map wrap vz411)",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' vz3 (wrap vz40 : [])",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="mergesort' vz3 (merge_pairs vz3 (wrap vz40 : wrap vz410 : map wrap vz411))",fontsize=16,color="black",shape="box"];17 -> 19[label="",style="solid", color="black", weight=3];
18[label="wrap vz40",fontsize=16,color="black",shape="triangle"];18 -> 20[label="",style="solid", color="black", weight=3];
19 -> 260[label="",style="dashed", color="red", weight=0];
19[label="mergesort' vz3 (merge vz3 (wrap vz40) (wrap vz410) : merge_pairs vz3 (map wrap vz411))",fontsize=16,color="magenta"];19 -> 261[label="",style="dashed", color="magenta", weight=3];
19 -> 262[label="",style="dashed", color="magenta", weight=3];
19 -> 263[label="",style="dashed", color="magenta", weight=3];
20[label="vz40 : []",fontsize=16,color="green",shape="box"];261 -> 492[label="",style="dashed", color="red", weight=0];
261[label="merge vz3 (wrap vz40) (wrap vz410)",fontsize=16,color="magenta"];261 -> 493[label="",style="dashed", color="magenta", weight=3];
261 -> 494[label="",style="dashed", color="magenta", weight=3];
262[label="vz3",fontsize=16,color="green",shape="box"];263[label="map wrap vz411",fontsize=16,color="burlywood",shape="triangle"];578[label="vz411/vz4110 : vz4111",fontsize=10,color="white",style="solid",shape="box"];263 -> 578[label="",style="solid", color="burlywood", weight=9];
578 -> 495[label="",style="solid", color="burlywood", weight=3];
579[label="vz411/[]",fontsize=10,color="white",style="solid",shape="box"];263 -> 579[label="",style="solid", color="burlywood", weight=9];
579 -> 496[label="",style="solid", color="burlywood", weight=3];
260[label="mergesort' vz36 (vz37 : merge_pairs vz36 vz38)",fontsize=16,color="burlywood",shape="triangle"];580[label="vz38/vz380 : vz381",fontsize=10,color="white",style="solid",shape="box"];260 -> 580[label="",style="solid", color="burlywood", weight=9];
580 -> 497[label="",style="solid", color="burlywood", weight=3];
581[label="vz38/[]",fontsize=10,color="white",style="solid",shape="box"];260 -> 581[label="",style="solid", color="burlywood", weight=9];
581 -> 498[label="",style="solid", color="burlywood", weight=3];
493 -> 18[label="",style="dashed", color="red", weight=0];
493[label="wrap vz410",fontsize=16,color="magenta"];493 -> 499[label="",style="dashed", color="magenta", weight=3];
494 -> 18[label="",style="dashed", color="red", weight=0];
494[label="wrap vz40",fontsize=16,color="magenta"];492[label="merge vz3 vz40 vz39",fontsize=16,color="burlywood",shape="triangle"];584[label="vz39/vz390 : vz391",fontsize=10,color="white",style="solid",shape="box"];492 -> 584[label="",style="solid", color="burlywood", weight=9];
584 -> 500[label="",style="solid", color="burlywood", weight=3];
585[label="vz39/[]",fontsize=10,color="white",style="solid",shape="box"];492 -> 585[label="",style="solid", color="burlywood", weight=9];
585 -> 501[label="",style="solid", color="burlywood", weight=3];
495[label="map wrap (vz4110 : vz4111)",fontsize=16,color="black",shape="box"];495 -> 502[label="",style="solid", color="black", weight=3];
496[label="map wrap []",fontsize=16,color="black",shape="box"];496 -> 503[label="",style="solid", color="black", weight=3];
497[label="mergesort' vz36 (vz37 : merge_pairs vz36 (vz380 : vz381))",fontsize=16,color="burlywood",shape="box"];586[label="vz381/vz3810 : vz3811",fontsize=10,color="white",style="solid",shape="box"];497 -> 586[label="",style="solid", color="burlywood", weight=9];
586 -> 504[label="",style="solid", color="burlywood", weight=3];
587[label="vz381/[]",fontsize=10,color="white",style="solid",shape="box"];497 -> 587[label="",style="solid", color="burlywood", weight=9];
587 -> 505[label="",style="solid", color="burlywood", weight=3];
498[label="mergesort' vz36 (vz37 : merge_pairs vz36 [])",fontsize=16,color="black",shape="box"];498 -> 506[label="",style="solid", color="black", weight=3];
499[label="vz410",fontsize=16,color="green",shape="box"];500[label="merge vz3 vz40 (vz390 : vz391)",fontsize=16,color="burlywood",shape="box"];588[label="vz40/vz400 : vz401",fontsize=10,color="white",style="solid",shape="box"];500 -> 588[label="",style="solid", color="burlywood", weight=9];
588 -> 507[label="",style="solid", color="burlywood", weight=3];
589[label="vz40/[]",fontsize=10,color="white",style="solid",shape="box"];500 -> 589[label="",style="solid", color="burlywood", weight=9];
589 -> 508[label="",style="solid", color="burlywood", weight=3];
501[label="merge vz3 vz40 []",fontsize=16,color="black",shape="box"];501 -> 509[label="",style="solid", color="black", weight=3];
502[label="wrap vz4110 : map wrap vz4111",fontsize=16,color="green",shape="box"];502 -> 510[label="",style="dashed", color="green", weight=3];
502 -> 511[label="",style="dashed", color="green", weight=3];
503[label="[]",fontsize=16,color="green",shape="box"];504[label="mergesort' vz36 (vz37 : merge_pairs vz36 (vz380 : vz3810 : vz3811))",fontsize=16,color="black",shape="box"];504 -> 512[label="",style="solid", color="black", weight=3];
505[label="mergesort' vz36 (vz37 : merge_pairs vz36 (vz380 : []))",fontsize=16,color="black",shape="box"];505 -> 513[label="",style="solid", color="black", weight=3];
506[label="mergesort' vz36 (vz37 : [])",fontsize=16,color="black",shape="box"];506 -> 514[label="",style="solid", color="black", weight=3];
507[label="merge vz3 (vz400 : vz401) (vz390 : vz391)",fontsize=16,color="black",shape="box"];507 -> 515[label="",style="solid", color="black", weight=3];
508[label="merge vz3 [] (vz390 : vz391)",fontsize=16,color="black",shape="box"];508 -> 516[label="",style="solid", color="black", weight=3];
509[label="vz40",fontsize=16,color="green",shape="box"];510 -> 18[label="",style="dashed", color="red", weight=0];
510[label="wrap vz4110",fontsize=16,color="magenta"];510 -> 517[label="",style="dashed", color="magenta", weight=3];
511 -> 263[label="",style="dashed", color="red", weight=0];
511[label="map wrap vz4111",fontsize=16,color="magenta"];511 -> 518[label="",style="dashed", color="magenta", weight=3];
512 -> 519[label="",style="dashed", color="red", weight=0];
512[label="mergesort' vz36 (vz37 : merge vz36 vz380 vz3810 : merge_pairs vz36 vz3811)",fontsize=16,color="magenta"];512 -> 520[label="",style="dashed", color="magenta", weight=3];
513[label="mergesort' vz36 (vz37 : vz380 : [])",fontsize=16,color="black",shape="box"];513 -> 521[label="",style="solid", color="black", weight=3];
514[label="vz37",fontsize=16,color="green",shape="box"];515 -> 522[label="",style="dashed", color="red", weight=0];
515[label="merge0 vz390 vz3 vz400 vz401 vz391 (vz3 vz400 vz390)",fontsize=16,color="magenta"];515 -> 523[label="",style="dashed", color="magenta", weight=3];
516[label="vz390 : vz391",fontsize=16,color="green",shape="box"];517[label="vz4110",fontsize=16,color="green",shape="box"];518[label="vz4111",fontsize=16,color="green",shape="box"];520 -> 492[label="",style="dashed", color="red", weight=0];
520[label="merge vz36 vz380 vz3810",fontsize=16,color="magenta"];520 -> 524[label="",style="dashed", color="magenta", weight=3];
520 -> 525[label="",style="dashed", color="magenta", weight=3];
520 -> 526[label="",style="dashed", color="magenta", weight=3];
519[label="mergesort' vz36 (vz37 : vz41 : merge_pairs vz36 vz3811)",fontsize=16,color="black",shape="triangle"];519 -> 527[label="",style="solid", color="black", weight=3];
521[label="mergesort' vz36 (merge_pairs vz36 (vz37 : vz380 : []))",fontsize=16,color="black",shape="box"];521 -> 528[label="",style="solid", color="black", weight=3];
523[label="vz3 vz400 vz390",fontsize=16,color="green",shape="box"];523 -> 534[label="",style="dashed", color="green", weight=3];
523 -> 535[label="",style="dashed", color="green", weight=3];
522[label="merge0 vz390 vz3 vz400 vz401 vz391 vz42",fontsize=16,color="burlywood",shape="triangle"];595[label="vz42/LT",fontsize=10,color="white",style="solid",shape="box"];522 -> 595[label="",style="solid", color="burlywood", weight=9];
595 -> 531[label="",style="solid", color="burlywood", weight=3];
596[label="vz42/EQ",fontsize=10,color="white",style="solid",shape="box"];522 -> 596[label="",style="solid", color="burlywood", weight=9];
596 -> 532[label="",style="solid", color="burlywood", weight=3];
597[label="vz42/GT",fontsize=10,color="white",style="solid",shape="box"];522 -> 597[label="",style="solid", color="burlywood", weight=9];
597 -> 533[label="",style="solid", color="burlywood", weight=3];
524[label="vz3810",fontsize=16,color="green",shape="box"];525[label="vz36",fontsize=16,color="green",shape="box"];526[label="vz380",fontsize=16,color="green",shape="box"];527[label="mergesort' vz36 (merge_pairs vz36 (vz37 : vz41 : merge_pairs vz36 vz3811))",fontsize=16,color="black",shape="box"];527 -> 536[label="",style="solid", color="black", weight=3];
528 -> 260[label="",style="dashed", color="red", weight=0];
528[label="mergesort' vz36 (merge vz36 vz37 vz380 : merge_pairs vz36 [])",fontsize=16,color="magenta"];528 -> 537[label="",style="dashed", color="magenta", weight=3];
528 -> 538[label="",style="dashed", color="magenta", weight=3];
534[label="vz400",fontsize=16,color="green",shape="box"];535[label="vz390",fontsize=16,color="green",shape="box"];531[label="merge0 vz390 vz3 vz400 vz401 vz391 LT",fontsize=16,color="black",shape="box"];531 -> 539[label="",style="solid", color="black", weight=3];
532[label="merge0 vz390 vz3 vz400 vz401 vz391 EQ",fontsize=16,color="black",shape="box"];532 -> 540[label="",style="solid", color="black", weight=3];
533[label="merge0 vz390 vz3 vz400 vz401 vz391 GT",fontsize=16,color="black",shape="box"];533 -> 541[label="",style="solid", color="black", weight=3];
536 -> 260[label="",style="dashed", color="red", weight=0];
536[label="mergesort' vz36 (merge vz36 vz37 vz41 : merge_pairs vz36 (merge_pairs vz36 vz3811))",fontsize=16,color="magenta"];536 -> 542[label="",style="dashed", color="magenta", weight=3];
536 -> 543[label="",style="dashed", color="magenta", weight=3];
537 -> 492[label="",style="dashed", color="red", weight=0];
537[label="merge vz36 vz37 vz380",fontsize=16,color="magenta"];537 -> 544[label="",style="dashed", color="magenta", weight=3];
537 -> 545[label="",style="dashed", color="magenta", weight=3];
537 -> 546[label="",style="dashed", color="magenta", weight=3];
538[label="[]",fontsize=16,color="green",shape="box"];539[label="vz400 : merge vz3 vz401 (vz390 : vz391)",fontsize=16,color="green",shape="box"];539 -> 547[label="",style="dashed", color="green", weight=3];
540[label="vz400 : merge vz3 vz401 (vz390 : vz391)",fontsize=16,color="green",shape="box"];540 -> 548[label="",style="dashed", color="green", weight=3];
541[label="vz390 : merge vz3 (vz400 : vz401) vz391",fontsize=16,color="green",shape="box"];541 -> 549[label="",style="dashed", color="green", weight=3];
542 -> 492[label="",style="dashed", color="red", weight=0];
542[label="merge vz36 vz37 vz41",fontsize=16,color="magenta"];542 -> 550[label="",style="dashed", color="magenta", weight=3];
542 -> 551[label="",style="dashed", color="magenta", weight=3];
542 -> 552[label="",style="dashed", color="magenta", weight=3];
543[label="merge_pairs vz36 vz3811",fontsize=16,color="burlywood",shape="triangle"];602[label="vz3811/vz38110 : vz38111",fontsize=10,color="white",style="solid",shape="box"];543 -> 602[label="",style="solid", color="burlywood", weight=9];
602 -> 553[label="",style="solid", color="burlywood", weight=3];
603[label="vz3811/[]",fontsize=10,color="white",style="solid",shape="box"];543 -> 603[label="",style="solid", color="burlywood", weight=9];
603 -> 554[label="",style="solid", color="burlywood", weight=3];
544[label="vz380",fontsize=16,color="green",shape="box"];545[label="vz36",fontsize=16,color="green",shape="box"];546[label="vz37",fontsize=16,color="green",shape="box"];547 -> 492[label="",style="dashed", color="red", weight=0];
547[label="merge vz3 vz401 (vz390 : vz391)",fontsize=16,color="magenta"];547 -> 555[label="",style="dashed", color="magenta", weight=3];
547 -> 556[label="",style="dashed", color="magenta", weight=3];
548 -> 492[label="",style="dashed", color="red", weight=0];
548[label="merge vz3 vz401 (vz390 : vz391)",fontsize=16,color="magenta"];548 -> 557[label="",style="dashed", color="magenta", weight=3];
548 -> 558[label="",style="dashed", color="magenta", weight=3];
549 -> 492[label="",style="dashed", color="red", weight=0];
549[label="merge vz3 (vz400 : vz401) vz391",fontsize=16,color="magenta"];549 -> 559[label="",style="dashed", color="magenta", weight=3];
549 -> 560[label="",style="dashed", color="magenta", weight=3];
550[label="vz41",fontsize=16,color="green",shape="box"];551[label="vz36",fontsize=16,color="green",shape="box"];552[label="vz37",fontsize=16,color="green",shape="box"];553[label="merge_pairs vz36 (vz38110 : vz38111)",fontsize=16,color="burlywood",shape="box"];607[label="vz38111/vz381110 : vz381111",fontsize=10,color="white",style="solid",shape="box"];553 -> 607[label="",style="solid", color="burlywood", weight=9];
607 -> 561[label="",style="solid", color="burlywood", weight=3];
608[label="vz38111/[]",fontsize=10,color="white",style="solid",shape="box"];553 -> 608[label="",style="solid", color="burlywood", weight=9];
608 -> 562[label="",style="solid", color="burlywood", weight=3];
554[label="merge_pairs vz36 []",fontsize=16,color="black",shape="box"];554 -> 563[label="",style="solid", color="black", weight=3];
555[label="vz390 : vz391",fontsize=16,color="green",shape="box"];556[label="vz401",fontsize=16,color="green",shape="box"];557[label="vz390 : vz391",fontsize=16,color="green",shape="box"];558[label="vz401",fontsize=16,color="green",shape="box"];559[label="vz391",fontsize=16,color="green",shape="box"];560[label="vz400 : vz401",fontsize=16,color="green",shape="box"];561[label="merge_pairs vz36 (vz38110 : vz381110 : vz381111)",fontsize=16,color="black",shape="box"];561 -> 564[label="",style="solid", color="black", weight=3];
562[label="merge_pairs vz36 (vz38110 : [])",fontsize=16,color="black",shape="box"];562 -> 565[label="",style="solid", color="black", weight=3];
563[label="[]",fontsize=16,color="green",shape="box"];564[label="merge vz36 vz38110 vz381110 : merge_pairs vz36 vz381111",fontsize=16,color="green",shape="box"];564 -> 566[label="",style="dashed", color="green", weight=3];
564 -> 567[label="",style="dashed", color="green", weight=3];
565[label="vz38110 : []",fontsize=16,color="green",shape="box"];566 -> 492[label="",style="dashed", color="red", weight=0];
566[label="merge vz36 vz38110 vz381110",fontsize=16,color="magenta"];566 -> 568[label="",style="dashed", color="magenta", weight=3];
566 -> 569[label="",style="dashed", color="magenta", weight=3];
566 -> 570[label="",style="dashed", color="magenta", weight=3];
567 -> 543[label="",style="dashed", color="red", weight=0];
567[label="merge_pairs vz36 vz381111",fontsize=16,color="magenta"];567 -> 571[label="",style="dashed", color="magenta", weight=3];
568[label="vz381110",fontsize=16,color="green",shape="box"];569[label="vz36",fontsize=16,color="green",shape="box"];570[label="vz38110",fontsize=16,color="green",shape="box"];571[label="vz381111",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz4110, vz4111), ba) → new_map(vz4111, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz4110, vz4111), ba) → new_map(vz4111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ RuleRemovalProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge(vz3, :(vz400, vz401), :(vz390, vz391), ba) → new_merge0(vz390, vz3, vz400, vz401, vz391, ba)
new_merge0(vz390, vz3, vz400, vz401, vz391, ba) → new_merge(vz3, :(vz400, vz401), vz391, ba)
new_merge0(vz390, vz3, vz400, vz401, vz391, ba) → new_merge(vz3, vz401, :(vz390, vz391), ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_merge(vz3, :(vz400, vz401), :(vz390, vz391), ba) → new_merge0(vz390, vz3, vz400, vz401, vz391, ba)

Used ordering: POLO with Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(new_merge(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(new_merge0(x₁, x₂, x₃, x₄, x₅, x₆)) = 2 + 2·x₁ + x₂ + 2·x₃ + x₄ + x₅ + x₆

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ RuleRemovalProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz390, vz3, vz400, vz401, vz391, ba) → new_merge(vz3, :(vz400, vz401), vz391, ba)
new_merge0(vz390, vz3, vz400, vz401, vz391, ba) → new_merge(vz3, vz401, :(vz390, vz391), ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(vz36, :(vz38110, :(vz381110, vz381111)), ba) → new_merge_pairs(vz36, vz381111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(vz36, :(vz38110, :(vz381110, vz381111)), ba) → new_merge_pairs(vz36, vz381111, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz36, vz37, vz41, vz3811, ba) → new_mergesort'0(vz36, new_merge1(vz36, vz37, vz41, ba), new_merge_pairs0(vz36, vz3811, ba), ba)
new_mergesort'0(vz36, vz37, :(vz380, :(vz3810, vz3811)), ba) → new_mergesort'(vz36, vz37, new_merge1(vz36, vz380, vz3810, ba), vz3811, ba)
new_mergesort'0(vz36, vz37, :(vz380, []), ba) → new_mergesort'0(vz36, new_merge1(vz36, vz37, vz380, ba), [], ba)

The TRS R consists of the following rules:

new_merge_pairs0(vz36, :(vz38110, []), ba) → :(vz38110, [])
new_merge_pairs0(vz36, [], ba) → []
new_merge_pairs0(vz36, :(vz38110, :(vz381110, vz381111)), ba) → :(new_merge1(vz36, vz38110, vz381110, ba), new_merge_pairs0(vz36, vz381111, ba))

The set Q consists of the following terms:

new_merge_pairs0(x0, [], x1)
new_merge_pairs0(x0, :(x1, []), x2)
new_merge_pairs0(x0, :(x1, :(x2, x3)), x4)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz36, vz37, vz41, vz3811, ba) → new_mergesort'0(vz36, new_merge1(vz36, vz37, vz41, ba), new_merge_pairs0(vz36, vz3811, ba), ba)
new_mergesort'0(vz36, vz37, :(vz380, :(vz3810, vz3811)), ba) → new_mergesort'(vz36, vz37, new_merge1(vz36, vz380, vz3810, ba), vz3811, ba)

The TRS R consists of the following rules:

new_merge_pairs0(vz36, :(vz38110, []), ba) → :(vz38110, [])
new_merge_pairs0(vz36, [], ba) → []
new_merge_pairs0(vz36, :(vz38110, :(vz381110, vz381111)), ba) → :(new_merge1(vz36, vz38110, vz381110, ba), new_merge_pairs0(vz36, vz381111, ba))

The set Q consists of the following terms:

new_merge_pairs0(x0, [], x1)
new_merge_pairs0(x0, :(x1, []), x2)
new_merge_pairs0(x0, :(x1, :(x2, x3)), x4)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'0(vz36, vz37, :(vz380, :(vz3810, vz3811)), ba) → new_mergesort'(vz36, vz37, new_merge1(vz36, vz380, vz3810, ba), vz3811, ba)

The remaining pairs can at least be oriented weakly.

new_mergesort'(vz36, vz37, vz41, vz3811, ba) → new_mergesort'0(vz36, new_merge1(vz36, vz37, vz41, ba), new_merge_pairs0(vz36, vz3811, ba), ba)

Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL([]) = 0
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge_pairs0(x₁, x₂, x₃)) = x₂
POL(new_mergesort'(x₁, x₂, x₃, x₄, x₅)) = x₄
POL(new_mergesort'0(x₁, x₂, x₃, x₄)) = x₃

The following usable rules [17] were oriented:

new_merge_pairs0(vz36, :(vz38110, []), ba) → :(vz38110, [])
new_merge_pairs0(vz36, :(vz38110, :(vz381110, vz381111)), ba) → :(new_merge1(vz36, vz38110, vz381110, ba), new_merge_pairs0(vz36, vz381111, ba))
new_merge_pairs0(vz36, [], ba) → []

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz36, vz37, vz41, vz3811, ba) → new_mergesort'0(vz36, new_merge1(vz36, vz37, vz41, ba), new_merge_pairs0(vz36, vz3811, ba), ba)

The TRS R consists of the following rules:

new_merge_pairs0(vz36, :(vz38110, []), ba) → :(vz38110, [])
new_merge_pairs0(vz36, [], ba) → []
new_merge_pairs0(vz36, :(vz38110, :(vz381110, vz381111)), ba) → :(new_merge1(vz36, vz38110, vz381110, ba), new_merge_pairs0(vz36, vz381111, ba))

The set Q consists of the following terms:

new_merge_pairs0(x0, [], x1)
new_merge_pairs0(x0, :(x1, []), x2)
new_merge_pairs0(x0, :(x1, :(x2, x3)), x4)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)